FDL - Nuprl Definition : equiv

Nuprl Definition : equiv_rel

12,41

compound
EquivRel(T;x,y.E(x;y)) == Refl(T;x,y.E(x;y)) & Sym(T;x,y.E(x;y)) & Trans(T;x,y.E(x;y))

Definitions Refl(T;x,y.E(x;y)), P & Q, Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y))

FDL editor aliases equiv_rel

Definitions	Refl(T;x,y.E(x;y)), P & Q, Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y))
FDL editor aliases	equiv_rel